Nuprl Lemma : qmul-zero-div
11,40
postcript
pdf
a
:
,
b
:
. ((0/
b
) *
a
) = 0
latex
Definitions
tt
,
if
b
then
t
else
f
fi
,
qeq(
r
;
s
)
,
P
Q
,
P
&
Q
,
P
Q
,
P
Q
,
(
r
/
s
)
,
,
t
T
,
x
:
A
.
B
(
x
)
,
,
S
T
Lemmas
neg
assert
of
eq
int
,
qmul
zero
qrng
,
qinv
wf
,
int
nzero
properties
,
int
nzero
wf
,
int
inc
rationals
,
qmul
wf
,
rationals
wf
origin
a:
, b:
. ((0/b) * a) = 0 
a:, b:. ((0/b) * a) = 0 
Q
Q Q
Tx:A. B(x)
T